\begin{tabbing}
es{-}bact\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$; $a$; ${\it es}$; $n$; $e_{1}$; $e_{2}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case \=TERMOF\{decidable\_\_ecl{-}es{-}act:ObjectId, 1:l, i:l\}\+\+
\\[0ex](${\it ds}$
\\[0ex],${\it da}$
\\[0ex],$a$
\\[0ex],${\it es}$
\\[0ex],loc($e_{1}$)
\\[0ex],$\lambda$$x$.axiom
\\[0ex],$\lambda$$x$,$y$. axiom
\\[0ex],$n$
\\[0ex],$e_{1}$
\\[0ex],$e_{2}$)
\-\\[0ex]o\=f inl($x$) =$>$ tt\+
\\[0ex]$\mid$ inr($x$) =$>$ ff
\-\-
\end{tabbing}